<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>EarleyParser</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="EarleyParser";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/EarleyItem.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/Grammar.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/EarleyParser.html" target="_top">Frames</a></li>
<li><a href="EarleyParser.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.verify</div>
<h2 title="Class EarleyParser" class="title">Class EarleyParser</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.verify.EarleyParser</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>All Implemented Interfaces:</dt>
<dd><a href="../../mmj/verify/GrammaticalParser.html" title="interface in mmj.verify">GrammaticalParser</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">EarleyParser</span>
extends java.lang.Object
implements <a href="../../mmj/verify/GrammaticalParser.html" title="interface in mmj.verify">GrammaticalParser</a></pre>
<div class="block">EarleyParser is my implementation of the Earley Parse algorithm, enhanced
 with Lookahead and various attempts at efficiency in Java.
 <p>
 The primary difference between this Earley Parser and the standard version is
 that input expressions are "pre-parsed" with variable hypotheses replacing
 the variables in the expression to be parsed. One reason for this change is
 that Var's and VarHyp's in Metamath are not necessarily in global scope;
 variable "x" might be a set now but later be a foobar. A drawback of this
 change is increased difficulty in building ParseTrees after EarleyParse
 finishes doing its "parse recognition" algorithm. Another drawback is that a
 restriction is placed on coding a grammatical Type Code, such as "wff" as a
 constant in a formula (ex. "xyz $a |- ( wff -> ph ) $." is prohibited because
 the "wff" is picked up as a something where a VarHyp should be...assuming the
 file that contains that statement uses "wff" as a Type Code.)
 <p>
 Another major change to the algorithm is that, while nulls and type
 conversions are handled in the mmj Grammar, a process of
 "combinatorial explosion" is used during the grammar-generation process, and
 so EarleyParser input "grammar" is solely the Notation Rules and unaltered
 VarHyp's. A grammar rule match to a subsequence of an expression may point to
 a Notation Rule that is a composite function of a Notation Syntax Axiom, plus
 any number of Nulls Permitted and Type Conversion Axioms; so when Earley is
 done, a fair amount of work still needs to happen to generate the output
 Parse tree/RPN for that match! It would definitely be feasible to revert the
 EarleyParse code to handle nulls and type conversions but extra invocations
 of Predictor and Completor are needed, as described in
 "Practical Techniques..." (see below) AND that still leaves the problem of
 how to generate an unambiguous grammar from a database like set.mm that
 contains "removable" or "non-essential ambiguities" such as overloaded
 functions.
 <p>
 The output of EarleyParser is an array of ParseTrees, and there is no
 arbitrary limit on the number of these trees in the event of ambiguity --
 except that imposed by the user in establishing the parseTreeArray. The
 sequence of the output trees *is* arbitrary however (I have no clue), but
 there are solid reasons to believe that duplicate trees will never be
 generated, under any circumstances.
 <p>
 The Earley Parse algorithm write-up talks incessantly about Item Sets. These
 are supposed to be actual *sets*, with no duplications in any one set. To
 accomplish that efficiently in Java was a coding issue. Instead of deleting
 duplicates after they are generated, I attempt to prevent generation of
 duplicate Earley Items in the first place using the pPredictorTyp and
 pBringForwardTyp arrays. And instead of coding the Item Sets as Java Sets I
 used arrays, pre-allocated for speed. The concession to quality is that I do
 do a duplicate check when adding an item to the pCompletedItem array -- no
 duplicates in that array means no duplicate Parse Trees, end of story
 (assuming the "build Parse Tree" logic isn't buggy.)
 <p>
 EarleyParser is my 3rd attempt at coding a parser capable of handling
 Metamath's set.mm database. BottomUpParser was my second attempt. Set.mm's
 "supeu" was too hairy for Bottom Up, but the algorithm does work -- when it
 actually gets around to computing an answer. My first attempt handled
 propositional logic just fine but died deep into set.mm and has since been
 deleted (not even a backup lives on...)
 <p>
 The nice thing about the Earley Parse algorithm is that it does handle all
 context free grammars and it does handle ambiguous grammars. If it works for
 set.mm then it is a helluva parser, because set.mm gives professional
 logicians gray hair with its intricate syntax!
 <p>
 See Dick Grune and Ceriel J.H. Jacob's "Parsing Techniques -- A Practical
 Guide", page 149 in Edition 1 -- which is the 139th page in the .pdf book
 file, available at:
 <p>
 <a href="http://www.cs.vu.nl/%7Edick/PTAPG.html"> Parsing Techniques -- A
 Practical Guide</a>
 <p>
 (Note: I went completely bald after working on this project. Fortunately,
 Dick Grune was incredibly friendly and helped me to understand some gnarly
 concepts. My hair may return, we shall see! While we're on the subject of
 heroes, Norm Megill has the patience of a saint. As far as I am concerned he
 is a prime candidate for the Nobel Prize. One day they will build statues of
 Norman Megill, and small boys will go to bed with Metamath bubble gum trading
 cards under their pillows...
 <p>
 <a href="../../EarleyParseFunctionAlgorithm.html">More on the Earley Parse
 Function Algorithm</a></div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/EarleyParser.html#EarleyParser(mmj.verify.Grammar, int)">EarleyParser</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammarIn,
            int&nbsp;maxFormulaLengthIn)</code>
<div class="block">Construct using reference to Grammar and a parameter signifying the
 maximum length of a formula in the database.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/EarleyParser.html#parseExpr(mmj.lang.ParseTree[], mmj.lang.Cnst, mmj.lang.ParseNodeHolder[], int)">parseExpr</a></strong>(<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>[]&nbsp;parseTreeArrayIn,
         <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;formulaTypIn,
         <a href="../../mmj/lang/ParseNodeHolder.html" title="class in mmj.lang">ParseNodeHolder</a>[]&nbsp;parseNodeHolderExprIn,
         int&nbsp;highestSeqIn)</code>
<div class="block">parseExpr - returns 'n' = the number of ParseTree objects generated for
 the input formula and stored in parseTreeArray.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="EarleyParser(mmj.verify.Grammar, int)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>EarleyParser</h4>
<pre>public&nbsp;EarleyParser(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammarIn,
            int&nbsp;maxFormulaLengthIn)</pre>
<div class="block">Construct using reference to Grammar and a parameter signifying the
 maximum length of a formula in the database.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammarIn</code> - Grammar object</dd><dd><code>maxFormulaLengthIn</code> - gives us a hint about what to expect.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="parseExpr(mmj.lang.ParseTree[], mmj.lang.Cnst, mmj.lang.ParseNodeHolder[], int)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>parseExpr</h4>
<pre>public&nbsp;int&nbsp;parseExpr(<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>[]&nbsp;parseTreeArrayIn,
            <a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;formulaTypIn,
            <a href="../../mmj/lang/ParseNodeHolder.html" title="class in mmj.lang">ParseNodeHolder</a>[]&nbsp;parseNodeHolderExprIn,
            int&nbsp;highestSeqIn)
              throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">parseExpr - returns 'n' = the number of ParseTree objects generated for
 the input formula and stored in parseTreeArray.
 <p>
 The user can control whether or not the first successful parse is
 returned by passing in an array of length = 1.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/verify/GrammaticalParser.html#parseExpr(mmj.lang.ParseTree[], mmj.lang.Cnst, mmj.lang.ParseNodeHolder[], int)">parseExpr</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/verify/GrammaticalParser.html" title="interface in mmj.verify">GrammaticalParser</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>parseTreeArrayIn</code> - holds generated ParseTrees, therefore, length
            must be greater than 0. The user can control whether or not
            the first successful parse is returned by passing in an array
            of length = 1. If the array length is greater than 1 the
            function attempts to fill the array with alternate parses
            (which if found, would indicate grammatical ambiguity.)
            Returned ParseTree objects are stored in array order -- 0, 1,
            2, ... -- and the contents of unused array entries is
            unspecified. If more than one ParseTree is returned, the
            returned ParseTrees are guaranteed to be different (no
            duplicate ParseTrees are returned!)</dd><dd><code>formulaTypIn</code> - Cnst Type Code of the Formula to be parsed.</dd><dd><code>parseNodeHolderExprIn</code> - Formula's Expression, preloaded into a
            ParseNodeHolder[] (see
            Formula(dot)getParseNodeHolderExpr(mandVarHypArray).</dd><dd><code>highestSeqIn</code> - restricts the parse to statements with a sequence
            number less than or equal to highestSeq. Set this to
            Integer(dot)MAX_VALUE to enable grammatical parsing using all
            available rules.</dd>
<dt><span class="strong">Returns:</span></dt><dd>int specifies the number of ParseTree objects stored into
         parseTreeArray; a number greater than 1 indicates grammatical
         ambiguity, by definition, since there is more than one way to
         parse the formula.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/EarleyItem.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/Grammar.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/EarleyParser.html" target="_top">Frames</a></li>
<li><a href="EarleyParser.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
